package ch.epfl.lara.matcheck.verify.spec;

import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.util.printer.PrettyStringerFormula
import ch.epfl.lara.matcheck.util.FreshName
import ch.epfl.lara.matcheck.verify.provers.ProverResults
import ch.epfl.lara.matcheck.verify.transform.ExtractorBody2Formula
import ch.epfl.lara.matcheck.verify.spec.exceptions._

import scala.collection.immutable.{Map,ListMap}

class DomainSpecVerifier extends SpecVerifier 
     with PropositionalFormulaMaker
{
  
  implicit def string2elem(name: String): Element = Element(name)
  
  private var _axioms: Formula = _
  private var _domains_to_verify: Formula = _
  private var _extractors: Map[String,ObjectDef] = _
  
  
  /** Constructor */
  def this(_domains_to_verify: Formula, 
      _extractors: Map[String,ObjectDef]) = {
      this()
      this._domains_to_verify = DomainDeclarationSimplifier(_domains_to_verify)
      this._extractors = _extractors
      this._axioms = AxiomsHolder.axiomsWithoutDomain
      verify(domains_to_verify)
  }
  
  
  /** Constructor */
  def this(domains_to_verify: Option[Formula], 
           extractors: Map[String,ObjectDef]) = {
    this(domains_to_verify.getOrElse(throw new DomainDeclarationEmpty),
         extractors)
  }
  
  /** Constructor */
  def this(domains_to_verify: Option[Formula], 
           objects: List[ObjectDef]) = {
    this(domains_to_verify,
         ListMap.empty ++ 
           (for(obj<-objects if obj.isExtractor) yield 
             (obj.getName,obj))
        )
           
  }
  
  
  //def verify() = verify(domains_to_verify)
  
    
  override def prove(setdomain: Formula): ProverResults.ProverResult = {
    val result = try { 
      append_axiom(domain2formula(setdomain.asInstanceOf[SubsetEq]))
      super.prove(Imply(axioms,setdomain))
    } catch {
      case RecursiveExtractor => setdomain.asInstanceOf[SubsetEq] match {
          case SubsetEq(left,set @ Set(name)) =>
            val z = FreshName.fresh("z")
            val extractor = domain2extractor(set)
            val method = extractor.getUnapply
            val param = method.params.head
            val (lhs,res) = ExtractorBody2Formula(method.body)
            val inductive_variables = CollectVariablesOfSet(name,lhs)
            val inductive_axioms = inductive_variables.foldLeft[Formula](Tru)((acc,x) => And(Imply(In(x,left),In(x,set)),acc))
            super.prove(Imply(axioms,
                              Imply(And(inductive_axioms,And(In(z,left),And(Eq(param.getName,z),lhs))), 
                                    res)))
            
          case _ => throw new Exception("Unsupported declaration")
        }
    }
    
    result match {
      case ProverResults.Valid => this._axioms = And(this._axioms,setdomain)
      case _ => ()
    }
    debug(setdomain,result)
    result
  }
  
  override protected def startTimer() {
    Timer.startProvingDomain()
  }
  
  override protected def stopTimer() {
    Timer.finishedProvingDomain()
  }
  
  private def debug(subset: Formula, result: ProverResults.ProverResult) {
    result match {
      case ProverResults.Invalid =>    
        Report.error("> "+PrettyStringerFormula(subset) + " is invalid.")
      case ProverResults.Timeout => 
        Report.error("> "+PrettyStringerFormula(subset) + " couldn't be verified. Prover Timeouts.")
      case ProverResults.Valid =>
        Report.verbose("> "+PrettyStringerFormula(subset) + " is valid.")
    }
    super.debug(last_formula_proved)
  }
  
  
  private def verify(f: Formula): ProverResults.ProverResult= f match {
    case And(l,r) => verify(l) && verify(r)
    case Or(l,r)  => verify(l) || verify(r)
    case subset: SubsetEq => prove(subset)
    case _ => 
      throw new Exception("Unexpected formula")
  }
  
  
  
  
  private def domain2formula(domain: Formula): Formula = domain match {
    
    case SubsetEq(EmptySet,right) => Tru          // by definition

    case SubsetEq(left,EmptySet) =>
      set2formula(left)
      
    case SubsetEq(left,set @ Set(name)) if hasRecursiveExtractor(set) =>
      throw RecursiveExtractor
      
    case SubsetEq(left,right) =>
      And(set2formula(left),
      set2formula(right))
      
    case _ => throw new Exception("error: the domain has not been simplified. Run DomainDeclarationSimplifier.")
  }
  
  private def hasRecursiveExtractor(set: Set): Boolean =  {
    val Set(name) = set
    if (!name.startsWith(Constants.DOM_PREPEND)) return false
    val extractor = domain2extractor(set)
    val method = extractor.getUnapply
    hasRecursiveExtractor(name.substring(Constants.DOM_PREPEND.length()),method.body)
  }
  
  private def hasRecursiveExtractor(extr_name: String, body: Expr): Boolean = body match {
    case Match(_,_,cases) => 
      for(CaseDef(_,p,_,b)<-cases) 
        if(hasRecursiveExtractor(extr_name,p) || hasRecursiveExtractor(extr_name,b)) return true
      false
    case If(_,then,elze) => hasRecursiveExtractor(extr_name,then) || hasRecursiveExtractor(extr_name,elze)
    case _ => false
  }
  
  private def hasRecursiveExtractor(extr_name: String, p: PatternDef): Boolean = p match {
    case VarPattern(_,_) | Wildcard => false
    case ClassPattern(name,args) =>
      if(name.getName == extr_name) return true
      else args.exists(hasRecursiveExtractor(extr_name,_))
  }
  
  import scala.collection.mutable.HashSet
  
  private var proved_domains: HashSet[String] = new HashSet[String]()
  
  private def set2formula(set: SetExpr): (Formula) = {
    
    def domainsOf(left: SetExpr, right: SetExpr): Formula = {
      And(iter(left),iter(right))
    }
    
    def iter(set: SetExpr): Formula = set match {
      case Union(left,right) => domainsOf(left,right)
        
      case Intersection(left,right) => domainsOf(left,right)
        
      case set @ Set(name) 
        if name.startsWith(Constants.DOM_PREPEND) && 
           !proved_domains.contains(name) =>
        
        proved_domains += (name)
        
        val binder = FreshName.fresh("x")
        val extractor = domain2extractor(set)
        val method = extractor.getUnapply
        val param = method.params.head
        val (lhs,res) = ExtractorBody2Formula(method.body)
        Equality(name,
                 SetComprehension(binder,
                 ExtractorBody2Formula.generated_fresh_names.foldRight[Formula]( 
                   Forall(param.getName,
                   Imply(And(Eq(param.getName,binder),lhs), 
                         And(In(binder,Set(param.getTpe)),res)))
                 )((local_name,f) => Forall(local_name,f))
                 ))
                      
      case set @ Set(name) => Tru
        
    }
    iter(set)
  }
  
  
  private def extractor(name: String): ObjectDef = extractors.get(name).get
  
  private def domain2extractor(set: Set): ObjectDef = 
    extractor(domain2extractorName(set))
  
  private def domain2extractorName(set: Set): String =
    set.name.substring(Constants.DOM_PREPEND.length())
    
  def axioms: Formula = _axioms        
  def append_axiom(a: Formula): Unit = _axioms = And(axioms,a)
  def domains_to_verify: Formula = _domains_to_verify
  def extractors      : Map[String,ObjectDef] = _extractors

}


object CollectVariablesOfSet {
  
  def apply(domset: String, f: Formula): List[String] = f match {
    case And(left,right) => this(domset,left) ::: this(domset,right)  
    case Or(left,right) =>  this(domset,left) ::: this(domset,right)
    case Imply(left,right) => this(domset,left) ::: this(domset,right)
    case Neg(f) => this(domset,f)
    case Equality(f1,f2) => this(domset,f1) ::: this(domset,f2) 
    case SetComprehension(_,f) => this(domset,f)
    case In(Element(name),Set(sname)) if sname == domset =>
      List(name)  
    case In(Element(name),set) =>
      Nil
    case Forall(x,f) =>  this(domset,f)
    case _ => Nil
  }
}
